perm filename ELEPHA.AX[S81,JMC] blob
sn#581743 filedate 1981-04-25 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 % elepha.ax[s81,jmc] Axioms for multiplication by addition in ELEPHANT
C00005 ENDMK
C⊗;
% elepha.ax[s81,jmc] Axioms for multiplication by addition in ELEPHANT
% Our object is to prove
% ∀t.(P(t) ∧ start ≤ pc(t) ≤ start+5 ⊃ pc(t+1) = done ∨ P(t+1))
% ⊃ ∀t0.(pc(t0) = start ∧ P(t0) ⊃
% ∃t2.(pc(t2) = done
% ∧ p(t2) = m*n
% ∧ ∀t1.(t0 ≤ t1 < t2 ⊃ P(t))))
% The induction is on the proposition
% Q(j) ≡
%
declare INDVAR j t t0 t1 t2 m m0 m1 m2 n n0 n1 n2 start done ε NATNUM;
declare OPCONST i(NATNUM) = NATNUM, p(NATNUM) = NATNUM, pc(NATNUM) = NATNUM;
% Inductive assertions schema
declare PREDPAR P 1 alldone 1;
declare OPPAR rank(GENERAL) =NATNUM;
axiom floyd:
∀t.(P(t) ∧ ¬alldone(t) ⊃ P(t+1) ∧ rank(t+1) < rank(t))
⊃ ∀t0.(P(t0) ⊃ ∃t2.(t0≤t2 ∧ alldone(t2) ∧ P(t2)
∧ ∀t1.(t0 ≤ t1 ∧ t1 < t2 ⊃ P(t1) ∧ ¬alldone(t1))))
;;
% fetch natnum.ax[s81,jmc];
axiom multprog:
∀t.(i(t+1) = IF pc(t) = start THEN n
ELSE IF pc(t) = start + 3 THEN i(t) - 1
ELSE IF start ≤ pc(t) ∧ pc(t) ≤ start + 5 THEN i(t)
ELSE i(t+1))
∀t.(p(t+1) =IF pc(t) = start + 1 THEN 0
ELSE IF pc(t) = start + 4 THEN p(t) + m
ELSE IF start ≤ pc(t) ∧ pc(t) ≤ start + 5 THEN p(t)
ELSE p(t+1))
∀t.(pc(t+1) = IF pc(t) = start + 2 ∧ i(t) = 0 THEN done
ELSE IF pc(t) = start + 5 THEN start + 2
ELSE IF start ≤ pc(t) ∧ pc(t) ≤ start + 5 THEN pc(t) + 1
ELSE pc(t+1))
;;
axiom foo:
∀j.(Q(j) ≡
∀t.(rank(t) ≤ j ⊃ (P(t) ∧ ¬alldone(t) ⊃ P(t+1) ∧ rank(t+1) < rank(t))
⊃ ∀t0.(P(t0) ⊃ ∃t2.(t0≤t2 ∧ alldone(t2) ∧ P(t2)
∧ ∀t1.(t0 ≤ t1 ∧ t1 < t2 ⊃ P(t1) ∧ ¬alldone(t1))))))
% Make a non-Zoharian temporal operator R such that Rp means that p
% will be true the next time we return to the present level after "pushes"
% and "pops".